p1(0) -> 0
p1(s1(X)) -> X
leq2(0, Y) -> true
leq2(s1(X), 0) -> false
leq2(s1(X), s1(Y)) -> leq2(X, Y)
if3(true, X, Y) -> activate1(X)
if3(false, X, Y) -> activate1(Y)
diff2(X, Y) -> if3(leq2(X, Y), n__0, n__s1(n__diff2(n__p1(X), Y)))
0 -> n__0
s1(X) -> n__s1(X)
diff2(X1, X2) -> n__diff2(X1, X2)
p1(X) -> n__p1(X)
activate1(n__0) -> 0
activate1(n__s1(X)) -> s1(activate1(X))
activate1(n__diff2(X1, X2)) -> diff2(activate1(X1), activate1(X2))
activate1(n__p1(X)) -> p1(activate1(X))
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
p1(0) -> 0
p1(s1(X)) -> X
leq2(0, Y) -> true
leq2(s1(X), 0) -> false
leq2(s1(X), s1(Y)) -> leq2(X, Y)
if3(true, X, Y) -> activate1(X)
if3(false, X, Y) -> activate1(Y)
diff2(X, Y) -> if3(leq2(X, Y), n__0, n__s1(n__diff2(n__p1(X), Y)))
0 -> n__0
s1(X) -> n__s1(X)
diff2(X1, X2) -> n__diff2(X1, X2)
p1(X) -> n__p1(X)
activate1(n__0) -> 0
activate1(n__s1(X)) -> s1(activate1(X))
activate1(n__diff2(X1, X2)) -> diff2(activate1(X1), activate1(X2))
activate1(n__p1(X)) -> p1(activate1(X))
activate1(X) -> X
ACTIVATE1(n__0) -> 01
DIFF2(X, Y) -> IF3(leq2(X, Y), n__0, n__s1(n__diff2(n__p1(X), Y)))
IF3(true, X, Y) -> ACTIVATE1(X)
ACTIVATE1(n__diff2(X1, X2)) -> DIFF2(activate1(X1), activate1(X2))
DIFF2(X, Y) -> LEQ2(X, Y)
ACTIVATE1(n__diff2(X1, X2)) -> ACTIVATE1(X1)
ACTIVATE1(n__s1(X)) -> S1(activate1(X))
ACTIVATE1(n__p1(X)) -> ACTIVATE1(X)
ACTIVATE1(n__diff2(X1, X2)) -> ACTIVATE1(X2)
LEQ2(s1(X), s1(Y)) -> LEQ2(X, Y)
IF3(false, X, Y) -> ACTIVATE1(Y)
ACTIVATE1(n__p1(X)) -> P1(activate1(X))
ACTIVATE1(n__s1(X)) -> ACTIVATE1(X)
p1(0) -> 0
p1(s1(X)) -> X
leq2(0, Y) -> true
leq2(s1(X), 0) -> false
leq2(s1(X), s1(Y)) -> leq2(X, Y)
if3(true, X, Y) -> activate1(X)
if3(false, X, Y) -> activate1(Y)
diff2(X, Y) -> if3(leq2(X, Y), n__0, n__s1(n__diff2(n__p1(X), Y)))
0 -> n__0
s1(X) -> n__s1(X)
diff2(X1, X2) -> n__diff2(X1, X2)
p1(X) -> n__p1(X)
activate1(n__0) -> 0
activate1(n__s1(X)) -> s1(activate1(X))
activate1(n__diff2(X1, X2)) -> diff2(activate1(X1), activate1(X2))
activate1(n__p1(X)) -> p1(activate1(X))
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
ACTIVATE1(n__0) -> 01
DIFF2(X, Y) -> IF3(leq2(X, Y), n__0, n__s1(n__diff2(n__p1(X), Y)))
IF3(true, X, Y) -> ACTIVATE1(X)
ACTIVATE1(n__diff2(X1, X2)) -> DIFF2(activate1(X1), activate1(X2))
DIFF2(X, Y) -> LEQ2(X, Y)
ACTIVATE1(n__diff2(X1, X2)) -> ACTIVATE1(X1)
ACTIVATE1(n__s1(X)) -> S1(activate1(X))
ACTIVATE1(n__p1(X)) -> ACTIVATE1(X)
ACTIVATE1(n__diff2(X1, X2)) -> ACTIVATE1(X2)
LEQ2(s1(X), s1(Y)) -> LEQ2(X, Y)
IF3(false, X, Y) -> ACTIVATE1(Y)
ACTIVATE1(n__p1(X)) -> P1(activate1(X))
ACTIVATE1(n__s1(X)) -> ACTIVATE1(X)
p1(0) -> 0
p1(s1(X)) -> X
leq2(0, Y) -> true
leq2(s1(X), 0) -> false
leq2(s1(X), s1(Y)) -> leq2(X, Y)
if3(true, X, Y) -> activate1(X)
if3(false, X, Y) -> activate1(Y)
diff2(X, Y) -> if3(leq2(X, Y), n__0, n__s1(n__diff2(n__p1(X), Y)))
0 -> n__0
s1(X) -> n__s1(X)
diff2(X1, X2) -> n__diff2(X1, X2)
p1(X) -> n__p1(X)
activate1(n__0) -> 0
activate1(n__s1(X)) -> s1(activate1(X))
activate1(n__diff2(X1, X2)) -> diff2(activate1(X1), activate1(X2))
activate1(n__p1(X)) -> p1(activate1(X))
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
LEQ2(s1(X), s1(Y)) -> LEQ2(X, Y)
p1(0) -> 0
p1(s1(X)) -> X
leq2(0, Y) -> true
leq2(s1(X), 0) -> false
leq2(s1(X), s1(Y)) -> leq2(X, Y)
if3(true, X, Y) -> activate1(X)
if3(false, X, Y) -> activate1(Y)
diff2(X, Y) -> if3(leq2(X, Y), n__0, n__s1(n__diff2(n__p1(X), Y)))
0 -> n__0
s1(X) -> n__s1(X)
diff2(X1, X2) -> n__diff2(X1, X2)
p1(X) -> n__p1(X)
activate1(n__0) -> 0
activate1(n__s1(X)) -> s1(activate1(X))
activate1(n__diff2(X1, X2)) -> diff2(activate1(X1), activate1(X2))
activate1(n__p1(X)) -> p1(activate1(X))
activate1(X) -> X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LEQ2(s1(X), s1(Y)) -> LEQ2(X, Y)
POL( LEQ2(x1, x2) ) = max{0, x2 - 2}
POL( s1(x1) ) = x1 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
p1(0) -> 0
p1(s1(X)) -> X
leq2(0, Y) -> true
leq2(s1(X), 0) -> false
leq2(s1(X), s1(Y)) -> leq2(X, Y)
if3(true, X, Y) -> activate1(X)
if3(false, X, Y) -> activate1(Y)
diff2(X, Y) -> if3(leq2(X, Y), n__0, n__s1(n__diff2(n__p1(X), Y)))
0 -> n__0
s1(X) -> n__s1(X)
diff2(X1, X2) -> n__diff2(X1, X2)
p1(X) -> n__p1(X)
activate1(n__0) -> 0
activate1(n__s1(X)) -> s1(activate1(X))
activate1(n__diff2(X1, X2)) -> diff2(activate1(X1), activate1(X2))
activate1(n__p1(X)) -> p1(activate1(X))
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
ACTIVATE1(n__diff2(X1, X2)) -> ACTIVATE1(X1)
ACTIVATE1(n__p1(X)) -> ACTIVATE1(X)
ACTIVATE1(n__diff2(X1, X2)) -> ACTIVATE1(X2)
DIFF2(X, Y) -> IF3(leq2(X, Y), n__0, n__s1(n__diff2(n__p1(X), Y)))
IF3(false, X, Y) -> ACTIVATE1(Y)
IF3(true, X, Y) -> ACTIVATE1(X)
ACTIVATE1(n__diff2(X1, X2)) -> DIFF2(activate1(X1), activate1(X2))
ACTIVATE1(n__s1(X)) -> ACTIVATE1(X)
p1(0) -> 0
p1(s1(X)) -> X
leq2(0, Y) -> true
leq2(s1(X), 0) -> false
leq2(s1(X), s1(Y)) -> leq2(X, Y)
if3(true, X, Y) -> activate1(X)
if3(false, X, Y) -> activate1(Y)
diff2(X, Y) -> if3(leq2(X, Y), n__0, n__s1(n__diff2(n__p1(X), Y)))
0 -> n__0
s1(X) -> n__s1(X)
diff2(X1, X2) -> n__diff2(X1, X2)
p1(X) -> n__p1(X)
activate1(n__0) -> 0
activate1(n__s1(X)) -> s1(activate1(X))
activate1(n__diff2(X1, X2)) -> diff2(activate1(X1), activate1(X2))
activate1(n__p1(X)) -> p1(activate1(X))
activate1(X) -> X